Skip to content

convex_function generalized#1887

Open
mkerjean wants to merge 6 commits intomath-comp:masterfrom
mkerjean:convex_20260306
Open

convex_function generalized#1887
mkerjean wants to merge 6 commits intomath-comp:masterfrom
mkerjean:convex_20260306

Conversation

@mkerjean
Copy link
Collaborator

@mkerjean mkerjean commented Mar 6, 2026 •
edited by affeldt-aist
Loading

Motivation for this change

Generalization the definition of convex functions in convex.v, from a function f: R -> R^o for R: realType to a function f : E -> R^o, for R: numFieldType and E : convex_lmodType.

This will allow the use of convex_function in the statement of Hahn-Banach theorem, and more generally, the use of semi-norms as convex functions on instances of convextvsType.

fixes issue #1888

Co-authored-by: Reynald Affeldt reynald.affeldt@aist.go.jp

Checklist
  • added corresponding entries in CHANGELOG_UNRELEASED.md
  • added corresponding documentation in the headers

Reference: How to document

Merge policy

As a rule of thumb:

  • PRs with several commits that make sense individually and that
    all compile are preferentially merged into master.
  • PRs with disorganized commits are very likely to be squash-rebased.
Reminder to reviewers

@mkerjean mkerjean requested a review from hoheinzollern March 6, 2026 03:28
@mkerjean mkerjean marked this pull request as ready for review March 6, 2026 03:29
@affeldt-aist affeldt-aist marked this pull request as draft March 6, 2026 05:21
@affeldt-aist affeldt-aist marked this pull request as draft March 6, 2026 05:21
affeldt-aist and others added 5 commits March 11, 2026 15:16
@affeldt-aist
generalization
65e2002 
Co-authored-by: Marie Kerjean <marie.kerjean@cnrs.fr>
@affeldt-aist
fix
3932450
@mkerjean @affeldt-aist
convex_function generalized
c7d9ec4 
Co-authored-by: Reynald Affeldt <reynald.affeldt@aist.go.jp>
@affeldt-aist
mv convex
640b0ca
@affeldt-aist
simplification
3e26e7b
@affeldt-aist affeldt-aist marked this pull request as ready for review March 11, 2026 06:17
mkerjean
mkerjean commented Mar 11, 2026
View reviewed changes
Copy link
Collaborator Author

@mkerjean mkerjean left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

necessary generalisation and shortening of proofs

@affeldt-aist
Copy link
Member

affeldt-aist commented Mar 11, 2026

@t6s Since we are touching convex.v, maybe you may want to take a look.
This PR does not do much beyond a generalization, but it is needed if we want Hahn-Banach (PR #1889 wip) to use the convexity definitions from convex.v

@affeldt-aist affeldt-aist self-requested a review March 11, 2026 06:25
t6s
t6s reviewed Mar 11, 2026
View reviewed changes
theories/normedtype_theory/tvs.v

Local Open Scope convex_scope.

Let standard_ball_convex (x : R^o) (r : R) : convex (ball x r).
Copy link
Member

@t6s t6s Mar 11, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Isn't this an instance of ball_convex above?

Copy link
Member

@affeldt-aist affeldt-aist Mar 11, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes but ball_convex is proved inside an HB builder where the carrier is an lmodType and has a norm,
but outside the builder we do not have such a structure, making it impossible to factorize. :-(

@t6s
Copy link
Member

t6s commented Mar 11, 2026

@t6s Since we are touching convex.v, maybe you may want to take a look. This PR does not do much beyond a generalization, but it is needed if we want Hahn-Banach (PR #1889 wip) to use the convexity definitions from convex.v

Looks good as a generalization.
The short identifier convex looks a bit too general to mean "is a convex set", but that is not an issue of this PR.

@affeldt-aist
Copy link
Member

affeldt-aist commented Mar 11, 2026

What about convex_set?

@t6s
Copy link
Member

t6s commented Mar 11, 2026

What about convex_set?

That looks specific enough. Is that conformant with other names for predicates on sets?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@affeldt-aist affeldt-aist affeldt-aist approved these changes

@hoheinzollern hoheinzollern Awaiting requested review from hoheinzollern

+1 more reviewer

@t6s t6s t6s left review comments

Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@mkerjean @affeldt-aist @t6s